E:Type, pred?:(E(E + top)), e:E. ((first(e)))  (pred(e)  E) 

latex

Definitions	Type, t  T, top, left + right, x:AB(x), f(a), x:A. B(x), isl(x), b, b, A, P  Q, outl(x), pred(e), first(e), False, P  Q, decidable(P), x:A  B(x), P  Q, P  Q
Lemmas	not functionality wrt iff, assert of bnot, decidable assert, outl wf, not wf, assert wf, bnot wf, isl wf, top wf